0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 82 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 5 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 137 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 24 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 0 ms)
↳34 QDP
↳35 MRRProof (⇔, 62 ms)
↳36 QDP
↳37 PisEmptyProof (⇔, 0 ms)
↳38 YES
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
TE_IN_G(s(T8)) → U8_G(T8, llA_in_ga(T8, X32))
TE_IN_G(s(T8)) → LLA_IN_GA(T8, X32)
LLA_IN_GA(s(T16), .(X66, X67)) → U1_GA(T16, X66, X67, llA_in_ga(T16, X67))
LLA_IN_GA(s(T16), .(X66, X67)) → LLA_IN_GA(T16, X67)
TE_IN_G(s(T8)) → U9_G(T8, llA_in_ga(T8, T10))
U9_G(T8, llA_out_ga(T8, T10)) → U10_G(T8, selectF_in_aaga(X5, X31, T10, X6))
U9_G(T8, llA_out_ga(T8, T10)) → SELECTF_IN_AAGA(X5, X31, T10, X6)
SELECTF_IN_AAGA(X131, X132, T34, .(X132, X133)) → U7_AAGA(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
SELECTF_IN_AAGA(X131, X132, T34, .(X132, X133)) → SELECTB_IN_AGA(X131, T34, X133)
SELECTB_IN_AGA(X168, .(T45, T47), .(T45, X169)) → U2_AGA(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
SELECTB_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTB_IN_AGA(X168, T47, X169)
U9_G(T8, llA_out_ga(T8, T10)) → U11_G(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_G(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_G(T8, pD_in_ag(X7, T21))
U11_G(T8, selectF_out_aaga(T19, T20, T10, T21)) → PD_IN_AG(X7, T21)
PD_IN_AG(X7, T21) → U4_AG(X7, T21, llC_in_ag(X7, T21))
PD_IN_AG(X7, T21) → LLC_IN_AG(X7, T21)
LLC_IN_AG(s(X221), .(T72, T74)) → U3_AG(X221, T72, T74, llC_in_ag(X221, T74))
LLC_IN_AG(s(X221), .(T72, T74)) → LLC_IN_AG(X221, T74)
PD_IN_AG(T61, T21) → U5_AG(T61, T21, llC_in_ag(T61, T21))
U5_AG(T61, T21, llC_out_ag(T61, T21)) → U6_AG(T61, T21, tE_in_g(T61))
U5_AG(T61, T21, llC_out_ag(T61, T21)) → TE_IN_G(T61)
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
TE_IN_G(s(T8)) → U8_G(T8, llA_in_ga(T8, X32))
TE_IN_G(s(T8)) → LLA_IN_GA(T8, X32)
LLA_IN_GA(s(T16), .(X66, X67)) → U1_GA(T16, X66, X67, llA_in_ga(T16, X67))
LLA_IN_GA(s(T16), .(X66, X67)) → LLA_IN_GA(T16, X67)
TE_IN_G(s(T8)) → U9_G(T8, llA_in_ga(T8, T10))
U9_G(T8, llA_out_ga(T8, T10)) → U10_G(T8, selectF_in_aaga(X5, X31, T10, X6))
U9_G(T8, llA_out_ga(T8, T10)) → SELECTF_IN_AAGA(X5, X31, T10, X6)
SELECTF_IN_AAGA(X131, X132, T34, .(X132, X133)) → U7_AAGA(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
SELECTF_IN_AAGA(X131, X132, T34, .(X132, X133)) → SELECTB_IN_AGA(X131, T34, X133)
SELECTB_IN_AGA(X168, .(T45, T47), .(T45, X169)) → U2_AGA(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
SELECTB_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTB_IN_AGA(X168, T47, X169)
U9_G(T8, llA_out_ga(T8, T10)) → U11_G(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_G(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_G(T8, pD_in_ag(X7, T21))
U11_G(T8, selectF_out_aaga(T19, T20, T10, T21)) → PD_IN_AG(X7, T21)
PD_IN_AG(X7, T21) → U4_AG(X7, T21, llC_in_ag(X7, T21))
PD_IN_AG(X7, T21) → LLC_IN_AG(X7, T21)
LLC_IN_AG(s(X221), .(T72, T74)) → U3_AG(X221, T72, T74, llC_in_ag(X221, T74))
LLC_IN_AG(s(X221), .(T72, T74)) → LLC_IN_AG(X221, T74)
PD_IN_AG(T61, T21) → U5_AG(T61, T21, llC_in_ag(T61, T21))
U5_AG(T61, T21, llC_out_ag(T61, T21)) → U6_AG(T61, T21, tE_in_g(T61))
U5_AG(T61, T21, llC_out_ag(T61, T21)) → TE_IN_G(T61)
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
LLC_IN_AG(s(X221), .(T72, T74)) → LLC_IN_AG(X221, T74)
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
LLC_IN_AG(s(X221), .(T72, T74)) → LLC_IN_AG(X221, T74)
LLC_IN_AG(.(T74)) → LLC_IN_AG(T74)
From the DPs we obtained the following set of size-change graphs:
SELECTB_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTB_IN_AGA(X168, T47, X169)
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
SELECTB_IN_AGA(X168, .(T45, T47), .(T45, X169)) → SELECTB_IN_AGA(X168, T47, X169)
SELECTB_IN_AGA(.(T47)) → SELECTB_IN_AGA(T47)
From the DPs we obtained the following set of size-change graphs:
LLA_IN_GA(s(T16), .(X66, X67)) → LLA_IN_GA(T16, X67)
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
LLA_IN_GA(s(T16), .(X66, X67)) → LLA_IN_GA(T16, X67)
LLA_IN_GA(s(T16)) → LLA_IN_GA(T16)
From the DPs we obtained the following set of size-change graphs:
TE_IN_G(s(T8)) → U9_G(T8, llA_in_ga(T8, T10))
U9_G(T8, llA_out_ga(T8, T10)) → U11_G(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_G(T8, selectF_out_aaga(T19, T20, T10, T21)) → PD_IN_AG(X7, T21)
PD_IN_AG(T61, T21) → U5_AG(T61, T21, llC_in_ag(T61, T21))
U5_AG(T61, T21, llC_out_ag(T61, T21)) → TE_IN_G(T61)
tE_in_g(s(T8)) → U8_g(T8, llA_in_ga(T8, X32))
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U8_g(T8, llA_out_ga(T8, X32)) → tE_out_g(s(T8))
tE_in_g(s(T8)) → U9_g(T8, llA_in_ga(T8, T10))
U9_g(T8, llA_out_ga(T8, T10)) → U10_g(T8, selectF_in_aaga(X5, X31, T10, X6))
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
U10_g(T8, selectF_out_aaga(X5, X31, T10, X6)) → tE_out_g(s(T8))
U9_g(T8, llA_out_ga(T8, T10)) → U11_g(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_g(T8, selectF_out_aaga(T19, T20, T10, T21)) → U12_g(T8, pD_in_ag(X7, T21))
pD_in_ag(X7, T21) → U4_ag(X7, T21, llC_in_ag(X7, T21))
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
U4_ag(X7, T21, llC_out_ag(X7, T21)) → pD_out_ag(X7, T21)
pD_in_ag(T61, T21) → U5_ag(T61, T21, llC_in_ag(T61, T21))
U5_ag(T61, T21, llC_out_ag(T61, T21)) → U6_ag(T61, T21, tE_in_g(T61))
tE_in_g(0) → tE_out_g(0)
U6_ag(T61, T21, tE_out_g(T61)) → pD_out_ag(T61, T21)
U12_g(T8, pD_out_ag(X7, T21)) → tE_out_g(s(T8))
TE_IN_G(s(T8)) → U9_G(T8, llA_in_ga(T8, T10))
U9_G(T8, llA_out_ga(T8, T10)) → U11_G(T8, selectF_in_aaga(T19, T20, T10, T21))
U11_G(T8, selectF_out_aaga(T19, T20, T10, T21)) → PD_IN_AG(X7, T21)
PD_IN_AG(T61, T21) → U5_AG(T61, T21, llC_in_ag(T61, T21))
U5_AG(T61, T21, llC_out_ag(T61, T21)) → TE_IN_G(T61)
llA_in_ga(s(T16), .(X66, X67)) → U1_ga(T16, X66, X67, llA_in_ga(T16, X67))
llA_in_ga(0, []) → llA_out_ga(0, [])
selectF_in_aaga(X131, X132, T34, .(X132, X133)) → U7_aaga(X131, X132, T34, X133, selectB_in_aga(X131, T34, X133))
selectF_in_aaga(X193, X193, T58, T58) → selectF_out_aaga(X193, X193, T58, T58)
llC_in_ag(s(X221), .(T72, T74)) → U3_ag(X221, T72, T74, llC_in_ag(X221, T74))
llC_in_ag(0, []) → llC_out_ag(0, [])
U1_ga(T16, X66, X67, llA_out_ga(T16, X67)) → llA_out_ga(s(T16), .(X66, X67))
U7_aaga(X131, X132, T34, X133, selectB_out_aga(X131, T34, X133)) → selectF_out_aaga(X131, X132, T34, .(X132, X133))
U3_ag(X221, T72, T74, llC_out_ag(X221, T74)) → llC_out_ag(s(X221), .(T72, T74))
selectB_in_aga(X168, .(T45, T47), .(T45, X169)) → U2_aga(X168, T45, T47, X169, selectB_in_aga(X168, T47, X169))
selectB_in_aga(T54, .(T54, T55), T55) → selectB_out_aga(T54, .(T54, T55), T55)
U2_aga(X168, T45, T47, X169, selectB_out_aga(X168, T47, X169)) → selectB_out_aga(X168, .(T45, T47), .(T45, X169))
TE_IN_G(s(T8)) → U9_G(llA_in_ga(T8))
U9_G(llA_out_ga(T10)) → U11_G(selectF_in_aaga(T10))
U11_G(selectF_out_aaga(T21)) → PD_IN_AG(T21)
PD_IN_AG(T21) → U5_AG(llC_in_ag(T21))
U5_AG(llC_out_ag(T61)) → TE_IN_G(T61)
llA_in_ga(s(T16)) → U1_ga(llA_in_ga(T16))
llA_in_ga(0) → llA_out_ga([])
selectF_in_aaga(T34) → U7_aaga(selectB_in_aga(T34))
selectF_in_aaga(T58) → selectF_out_aaga(T58)
llC_in_ag(.(T74)) → U3_ag(llC_in_ag(T74))
llC_in_ag([]) → llC_out_ag(0)
U1_ga(llA_out_ga(X67)) → llA_out_ga(.(X67))
U7_aaga(selectB_out_aga(X133)) → selectF_out_aaga(.(X133))
U3_ag(llC_out_ag(X221)) → llC_out_ag(s(X221))
selectB_in_aga(.(T47)) → U2_aga(selectB_in_aga(T47))
selectB_in_aga(.(T55)) → selectB_out_aga(T55)
U2_aga(selectB_out_aga(X169)) → selectB_out_aga(.(X169))
llA_in_ga(x0)
selectF_in_aaga(x0)
llC_in_ag(x0)
U1_ga(x0)
U7_aaga(x0)
U3_ag(x0)
selectB_in_aga(x0)
U2_aga(x0)
TE_IN_G(s(T8)) → U9_G(llA_in_ga(T8))
U9_G(llA_out_ga(T10)) → U11_G(selectF_in_aaga(T10))
U11_G(selectF_out_aaga(T21)) → PD_IN_AG(T21)
PD_IN_AG(T21) → U5_AG(llC_in_ag(T21))
U5_AG(llC_out_ag(T61)) → TE_IN_G(T61)
llA_in_ga(s(T16)) → U1_ga(llA_in_ga(T16))
llA_in_ga(0) → llA_out_ga([])
selectF_in_aaga(T34) → U7_aaga(selectB_in_aga(T34))
selectF_in_aaga(T58) → selectF_out_aaga(T58)
llC_in_ag(.(T74)) → U3_ag(llC_in_ag(T74))
llC_in_ag([]) → llC_out_ag(0)
U1_ga(llA_out_ga(X67)) → llA_out_ga(.(X67))
U7_aaga(selectB_out_aga(X133)) → selectF_out_aaga(.(X133))
U3_ag(llC_out_ag(X221)) → llC_out_ag(s(X221))
selectB_in_aga(.(T47)) → U2_aga(selectB_in_aga(T47))
selectB_in_aga(.(T55)) → selectB_out_aga(T55)
U2_aga(selectB_out_aga(X169)) → selectB_out_aga(.(X169))
PDINAG1 > selectFinaaga1 > U9G1 > llCinag1 > U7aaga1 > s1 > selectFoutaaga1 > U5AG1 > selectBinaga1 > U11G1 > 0 > TEING1 > U2aga1 > selectBoutaga1 > [] > llAinga1 > U3ag1 > llCoutag1 > .1 > U1ga1 > llAoutga1
0=2
[]=1
llA_in_ga_1=7
s_1=6
U1_ga_1=6
llA_out_ga_1=8
selectF_in_aaga_1=9
U7_aaga_1=6
selectB_in_aga_1=2
selectF_out_aaga_1=7
llC_in_ag_1=9
._1=6
U3_ag_1=6
llC_out_ag_1=7
selectB_out_aga_1=7
U2_aga_1=6
TE_IN_G_1=7
U9_G_1=5
U11_G_1=4
PD_IN_AG_1=10
U5_AG_1=1
llA_in_ga(x0)
selectF_in_aaga(x0)
llC_in_ag(x0)
U1_ga(x0)
U7_aaga(x0)
U3_ag(x0)
selectB_in_aga(x0)
U2_aga(x0)